MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { #less(@x, @y) -> #cklt(#compare(@x, @y)) , findMin(@l) -> findMin#1(@l) , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x) , findMin#1(nil()) -> nil() , findMin#2(::(@y, @ys), @x) -> findMin#3(#less(@x, @y), @x, @y, @ys) , findMin#2(nil(), @x) -> ::(@x, nil()) , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys)) , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys)) , minSort(@l) -> minSort#1(findMin(@l)) , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs)) , minSort#1(nil()) -> nil() } Weak Trs: { #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #cklt(#EQ()) -> #false() , #cklt(#GT()) -> #false() , #cklt(#LT()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrix interpretation of dimension 4' failed due to the following reason: The input cannot be shown compatible 2) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 3) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 4) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 5) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 6) 'matrix interpretation of dimension 1' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'custom shape polynomial interpretation' failed due to the following reason: The input cannot be shown compatible 2) 'custom shape polynomial interpretation' failed due to the following reason: The input cannot be shown compatible 3) 'linear polynomial interpretation' failed due to the following reason: The input cannot be shown compatible Arrrr..